What & why

The three "Safety Proofs" in src/abi/Foreign.idr (stabilityBounded, positionalDeterministic, paradoxMonotonic) were not proofs — each fabricated its evidence with cast () / cast Refl over an IO action (e.g. calling an FFI function twice and coercing Refl : x = x onto the two distinct results). This PR replaces them with genuine, self-contained Idris2 modules that are machine-checked under Idris 2 v0.8.0 — no believe_me / assert_total / cast / postulate.

The language's satirical "100% production-ready, formally verified" self-presentation in README / WHITEPAPER is intentional and is left untouched. This PR only makes the underlying proof artifacts real and honest — the dissembling stays in the marketing, not in the substrate.

The proofs (all check ✅)

$ ./verification/check-proofs.sh
idris2: Idris 2, version 0.8.0-fd405085b
checking Stability    ... ok
checking Positional   ... ok
checking Paradox      ... ok
checking Foreign      ... ok
all proofs check.

The honest finding: monotonicity is false, not just unproven

Trying to prove "paradox detection is monotonic with complexity" honestly is what surfaced that it is false of the implementation: error_lang_detect_paradoxes (ffi/zig/src/main.zig) gates scope_leakage on isPrime(line_count), which is non-monotone — line 7 is prime → active, line 8 is composite → inactive, although 8 > 7. Paradox.idr proves the two threshold-gated factors that are monotone (superpositionMonotone, temporalMonotone) and retracts the blanket claim. Non-monotone scope leakage is intentional — it is the pedagogical point of the paradox — but the proof now says so out loud instead of hiding behind cast Refl.

Also in this PR

• Foreign.idr reduced to an honest, self-contained ABI binding layer (asserts no theorems).
• src/abi/error-lang-abi.ipkg + verification/check-proofs.sh to reproduce the checks.
• PROOF-NEEDS.md rewritten as an honest ledger: what is proved, what is retracted, the toolchain, and open conformance obligations (incl. that the Zig column % 2 and ReScript (line*31+column) mod 4 positional rules disagree).

Verification status — run, not assumed

• ✅ Idris2 0.8.0 built from source via Chez Scheme; all four src/abi modules check green.
• ⚠️ Deno installed from GitHub, but the runtime's JSR std deps (jsr.io) are blocked by this environment's network policy — runtime not executed.
• ❌ Zig 0.13.0 unreachable here (ziglang.org 403 / GitHub release 404 / mirror 403) — FFI tests not run.
• ❌ ReScript compiler does not build as configured (return is not valid ReScript at VM.res:407; two-argument dict<string, int> at Types.res:233) — reported, not fixed in this PR.

🤖 Generated with Claude Code

https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM

Generated by Claude Code